﻿// Spun AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Formality.Levels;
using Formality.FormalSystem;

namespace Formality.Logic.Game
{
    public class Engine
    {
        public Engine()
        {
            Sentences = new FullEnumerator();
        }

        public Sentence this[string Id]
        {
            get
            {
                return (from S in Sentences
                        where S.Id == Id
                        select S).Single();
            }
        }

        public IEnumerable<Sentence> GetPremises(string Id)
        {
            return Sentences.TakeWhile(S => S.Id.Equals(Id) == false);
        }

        public string Next(string Id)
        {
            var Iterator = Sentences.GetEnumerator();

            while (Iterator.MoveNext())
                if (Iterator.Current.Id == Id)
                {
                    while (Iterator.MoveNext())
                    {
                        if (Iterator.Current is Proposition)
                            return Iterator.Current.Id;
                    }

                    return null;
                }

            throw new Exception("Could not find sentence with Id " + Id);
        }

        public Inference? Follows(Proposition Proposal, IEnumerable<Sentence> Priori)
        {
            foreach (var Basis in Priori)
            {
                var Inf = Basis.Implies(Proposal, Priori);

                if (Inf.HasValue)
                    return Inf;
            }

            return null;
        }

        private IEnumerable<Sentence> Sentences;
    }
}
